$\forall$$T$:Type, $j$:$\mathbb{N}$, $l$:($T$ List).
\\[0ex](0 $<$ $j$) $\Rightarrow$ ($j$ $\leq$ $\parallel$$l$$\parallel$) $\Rightarrow$ ((firstn($j$ {-} 1;$l$) @ [$l$[($j$ {-} 1)]]) $\sim$ firstn($j$;$l$))